#include <iostream>
#include <memory>

#include "NullFactory.h"
#include "BinaryNode.h"
#include "MultipleNode.h"
#include "Parser.h"
#include "Printer.h"
#include "NNFProcessor.h"
//#include "Traverser.h"

#include "Benchmark.h"
#include "BenchmarkParse.h"

const size_t giIterationsCount = 100000;

template<class Node>
void TestParse1(const std::string & sInput)
{
    std::cout << std::endl << "Parsing and printing (Node Type: " << Node::getNodeKind() << "): "<< sInput << std::endl;
    NodeFactory<Node> factory;
    std::auto_ptr<Node> pNode(parse<Node>(sInput, factory));
    
    std::cout << "Explicit Printed result: " << Printer<ExplicitPrinter>::print(pNode.get()) << std::endl;
    std::cout << "Pretty Printed result: " << Printer<PrettyPrinter>::print(pNode.get()) << std::endl;
    std::cout << "Postfix Printed result: " << Printer<PostfixPrinter>::print(pNode.get()) << std::endl;
}

template<class Node, class Factory>
void TestParse2(const std::string & sInput, const Factory & factory)
{
    std::cout << std::endl << "Parsing and printing (Node Type: " << Node::getNodeKind() << 
                              ", Factory Type: " << factory.getFactoryName() << "): "<< sInput << std::endl;
    std::auto_ptr<Node> pNode(parse<Node>(sInput, factory));
    std::cout << "Explicit Printed result: " << Printer<ExplicitPrinter>::print(pNode.get()) << std::endl;
}

template<class Node>
void TestConvertNNF(const std::string & sInput)
{
    std::cout << std::endl << "Converting to NNF..." << std::endl;
    NodeFactory<Node> factory;
    std::auto_ptr<Node> pNode(parse<Node>(sInput, factory));
    std::cout << "Parsed result: " << Printer<>::print(pNode.get()) << std::endl;
    bool bRes = inplaceProcessNNF(pNode, factory);
    std::cout << "Processed result (" << bRes << "): " << Printer<ExplicitPrinter>::print(pNode.get()) << std::endl;
}

int main(int argc, char ** argv)
{
    TestParse1<BinaryNode>("AB|C&~D|~~EF|&ABC&|~&~");
    TestParse1<MultipleNode>("AB|C&~D|~~EF|&ABC&|~&~");

    TestParse2<BinaryNode>("AB|C|ABC||&~AB&C&ABC&&|~&", NodeFactory<BinaryNode>());
    TestParse2<MultipleNode>("AB|C|", NodeFactory<MultipleNode>());
    TestParse2<MultipleNode>("ABC||", NodeFactory<MultipleNode>());
    TestParse2<MultipleNode>("AB&C&", NodeFactory<MultipleNode>());
    TestParse2<MultipleNode>("ABC&&", NodeFactory<MultipleNode>());
    TestParse2<MultipleNode>("AB|C|ABC||&~AB&C&ABC&&|~&", NodeFactory<MultipleNode>());
    TestParse2<MultipleNode>("AB|C|", VisitorNodeFactory());
    TestParse2<MultipleNode>("ABC||", VisitorNodeFactory());
    TestParse2<MultipleNode>("AB&C&", VisitorNodeFactory());
    TestParse2<MultipleNode>("ABC&&", VisitorNodeFactory());
    TestParse2<MultipleNode>("AB|C|ABC||&~AB&C&ABC&&|~&", VisitorNodeFactory());

    TestConvertNNF<BinaryNode>("AB&C&~");
    TestConvertNNF<MultipleNode>("AB&C&~");

/*
    bool bRes;
    // testing with ApplyOnce policy
    std::auto_ptr<INode> pNewNode(pNode->clone());
    std::cout << "Normalizing: " << pNewNode->print() << std::endl;
    bRes = Traverse<ApplyOnce>(pNewNode, NNFProcessor(bf));
    std::cout << "Processing result (" << bRes << "): " << pNewNode->print() << std::endl;
    bRes = Traverse<ApplyOnce>(pNewNode, NNFProcessor(bf));
    std::cout << "Processing result (" << bRes << "): " << pNewNode->print() << std::endl;
    bRes = Traverse<ApplyOnce>(pNewNode, NNFProcessor(bf));
    std::cout << "Processing result (" << bRes << "): " << pNewNode->print() << std::endl;
    bRes = Traverse<ApplyOnce>(pNewNode, NNFProcessor(bf));
    std::cout << "Processing result (" << bRes << "): " << pNewNode->print() << std::endl;

    // testing with ApplyUntilUnchanged policy
    pNewNode.reset(pNode->clone());
    std::cout << "Normalizing: " << pNewNode->print() << std::endl;
    bRes = Traverse<ApplyUntilUnchanged>(pNewNode, NNFProcessor(bf));
    std::cout << "Processing result (" << bRes << "): " << pNewNode->print() << std::endl;
    bRes = Traverse<ApplyUntilUnchanged>(pNewNode, NNFProcessor(bf));
    std::cout << "Processing result (" << bRes << "): " << pNewNode->print() << std::endl;
    bRes = Traverse<ApplyUntilUnchanged>(pNewNode, NNFProcessor(bf));
    std::cout << "Processing result (" << bRes << "): " << pNewNode->print() << std::endl;
    bRes = Traverse<ApplyUntilUnchanged>(pNewNode, NNFProcessor(bf));
    std::cout << "Processing result (" << bRes << "): " << pNewNode->print() << std::endl;
*/
/*
    std::auto_ptr<INode> pNewNode(Traverse(pNode.get(), NNFProcessor(bf)));
    std::cout << "Processed result: " << pNewNode->print() << std::endl;
    std::auto_ptr<INode> pNewNode2(Traverse(pNewNode.get(), NNFProcessor(bf)));
    std::cout << "Processed result: " << pNewNode2->print() << std::endl;
    std::auto_ptr<INode> pNewNode3(Traverse(pNewNode2.get(), NNFProcessor(bf)));
    std::cout << "Processed result: " << pNewNode3->print() << std::endl;
    std::auto_ptr<INode> pNewNode4(Traverse(pNewNode3.get(), NNFProcessor(bf)));
    std::cout << "Processed result: " << pNewNode4->print() << std::endl;
*/


    std::cout << std::endl << std::endl << "Running benchmarks" << std::endl;
//    std::string sInputString("AB|C&~D|~~EF|&");
    std::string sInputString("AB|C|ABC||&~AB&C&ABC&&|~&");
    benchmark(ParseBenchmark<BinaryNode>(sInputString), giIterationsCount);
    benchmark(ParseBenchmark<MultipleNode>(sInputString), giIterationsCount);
    benchmark(ParseBenchmark<MultipleNode, VisitorNodeFactory>(sInputString), giIterationsCount);
    benchmark(ParseBenchmark<NullNode>(sInputString), giIterationsCount);

    return 0;
}
